/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.api;

import java.io.BufferedReader;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;

import alloy.ast.Command;
import alloy.ast.Formula;
import alloy.ast.Id;
import alloy.ast.LeafExpr;
import alloy.ast.QualifiedName;
import alloy.ast.SigExpr;
import alloy.ast.Specification;
import alloy.bool.BooleanFormula;
import alloy.transform.FunctionSkolemizer;
import alloy.transl.ASTInfo;
import alloy.transl.ExprTransl;
import alloy.transl.TranslInfo;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.util.AlloyConstants;
import alloy.util.Dbg;
import alloy.viz.alloyviz.VizInstance;

/**
 * A basic data structure that provides
 * an interface to information about a
 * solution to a particular command
 * in an Alloy model.  Creates all
 * data structures at initialization
 * time (a lazy implementation may
 * be better in some cases).
 */
class SolutionDataImpl implements SolutionData, AlloyConstants {

    /** a List of the signatures encountered in this
    solution */
    private List _sigs = new ArrayList();

    /** a Map from String signature names to their
    {@link BasicType basic types}. */
    private Map _sigsToBasicTypes = new HashMap();

    /** a Map from String signature names to Maps
    from the sig's String fields to the RelationTypes of
    the fields */
    private Map _sigsToFieldTypes = new HashMap();

    /** a Map from String signature names to Lists
    of String names of the atoms associated with
    that sig in this solution */
    private Map _sigsToAtoms = new HashMap();

    /** a Map from String atom names to the String signature
    name corresponding to its type */
    private Map _atomsToSigs = new HashMap();

    /** a Map from String relation names (signame$fieldname) to
    their {@link alloy.type.RelationType relation types}*/
    private Map _relationsToRelationTypes = new HashMap();

    /** a Map from String relation names (signame$fieldname) to
    Lists of String[] arrays of their tuples */
    private Map _relationsToTuples = new HashMap();

    /** a Map from String atom names to Maps from String
    relation names to String[] arrays of relation values
    after applying the relation to the original atom */
    private Map _atomsToRelationValues = new HashMap();

    /** a Map from skolem constant String names to their
    RelationType types */
    private Map _skolemToTypes = new TreeMap();

    /** a Map from skolem constant String names to
    a List of String[] arrays oftheir values */
    private Map _skolemToValues = new HashMap();

    /** a Map from String signature and skolem constant
    full names to either the same full name or a shortened
    name if shortening is possible */
//    private Map _nameToShortName = new HashMap();

    /** used to shorten names when possible */
    private NameShortener _shortener;

    /** The {@link TranslInfo} used during translation.  It can be queried for various
    summary information about the formula, e.g. the list of all relations.
    @see #getTranslator */
    private TranslInfo _translator;

    /** Assignment of Boolean variables to values */
    private boolean[] _solution;

    /** The desugared Alloy formula we were analyzing */
    private Formula _formula;

    /** The {@link Command} we were analyzing. */
    private Command _command;

    /** The translation of the formula we were analyzing */
    private BooleanFormula _translation;

    /** Specification of the model containing the command we were analyzing **/
    private Specification _spec;

    /** FunctionSkolemizer used to skolemize this._spec **/
    private FunctionSkolemizer _fs;

    private alloy.viz.alloyviz.VizInstance _instance;

    public SolutionDataImpl(
                TranslInfo translator_,
                boolean[] solution_,
                Formula formula_,
                Command command_,
                BooleanFormula translation_,
                Specification spec_,
                FunctionSkolemizer fs_) {
        // initialize data structures
        _translator = translator_;
        _solution = solution_;
        _formula = formula_;
        _command = command_;

            _translation = translation_;
        _spec = spec_;
        _fs = fs_;

        Map exprsToTransls = translator_.getRelationExprsToTransls();
        _shortener = new NameShortener(exprsToTransls);
        // handle sigs and skolem constants first
        _addSigsAndSkolemConstants(exprsToTransls, solution_);
        // then, handle fields (relations)
        _addFields(exprsToTransls, solution_);
    }

    //public String toString() {
    // just dump all the state
    /*StringBuffer ret = new StringBuffer("sigs: " + _sigs + "\n");
      ret.append("fields: " + _sigsToFieldTypes + "\n");
      ret.append("atoms: " + _sigsToAtoms + "\n");
      ret.append("mappings: " + _atomsToRelationValues + "\n");
      ret.append("skolem types: " + _skolemToTypes + "\n");
      ret.append("skolem values: " + _skolemToValues + "\n");
      return ret.toString();*/
    //ByteArrayOutputStream baos = new ByteArrayOutputStream();
    //_translator.interpretRelations(_solution, new PrintStream(baos));
    //return baos.toString();
    //}

    public List allTypes() {
        return new ArrayList(_translator.getBasicTypes());
    }

    /** get a list of all String signature names
    corresponding to types seen in the
    formula generated for a command */
    public List allSigs() {
        return _sigs;
    }

    public BasicType typeOfSig(String sigName_) {
        return (BasicType) _sigsToBasicTypes.get(sigName_);
    }

    public boolean isBasic(String sigName_) {
        return sigName_.equals(
                   _getShortName(typeOfSig(sigName_).toExpr().nodeString()));
    }

    public Map allRelations() {
        return _relationsToRelationTypes;
    }

    /** given the name of a signature, returns
    a mapping from the signature's String
    fields to their RelationType types */
    public Map fieldsOfSig(String sigName_) {
        return (Map) _sigsToFieldTypes.get(sigName_);
    }

    public List tuplesOfRelation(String relationName_) {
        return (List) _relationsToTuples.get(relationName_);
    }

    /** given the name of a signature, returns
    a list of String atom names seen in
    the set associated with that signature
    in the solution */
    public List atomsOfSig(String sigName_) {
        return (List) _sigsToAtoms.get(sigName_);
    }

    /** given the name of an atom, returns
    the String signature name associated
    with its type */
    public String typeOfAtom(String atomName_) {
        return (String) _atomsToSigs.get(atomName_);
    }

    /** given the name of an atom and the
    name of a relation mapping that atom,
    returns a List of String[] arrays
    corresponding to all tuples obtained
    by applying the relation to the atom
    in this solution */
    public List applyRelationToAtom(String atomName_, String relationName_) {
        Map relationToVals = (Map) _atomsToRelationValues.get(atomName_);
        Dbg.chk(relationToVals);
        return (List) relationToVals.get(relationName_);
    }

    /** get a Map from the String names of all
    skolem constants to their RelationType
    types */
    public Map skolemConstants() {
        return _skolemToTypes;
    }

    /** given the name of a skolem constant, returns
    a List of String[] arrays corresponding to
    the values of the skolem constant in this
    solution */
    public List skolemConstantValues(String skolemName_) {
        return (List) _skolemToValues.get(skolemName_);
    }

    /** @return the {@link TranslInfo} which translated the desugared alloy
    {@link alloy.ast.Formula} into a {@link alloy.bool.BooleanFormula}.  the
    {@link TranslInfo} accumulates some useful information during translation
    which can be retrieved afterwards, e.g. {@link TranslInfo#getNodeTranslations},
    {@link TranslInfo#getVarSwitches}, {@link TranslInfo#getRelationReps}, etc.*/
    public TranslInfo getTranslator() {
        return _translator;
    }

    public BooleanFormula getTranslation() {
        return _translation;
    }

    public Specification getSpecification() {
        return _spec;
    }

    public FunctionSkolemizer getSkolemizer() {
        return _fs;
    }

    public ASTInfo getASTInfo() { return _translator; }

    /** @return the assignment of values to Boolean variables. */
    public boolean[] getSolution() {
        return _solution;
    }

    /** @return the desugared Alloy {@link Formula} we were analyzing */
    public Formula getFormula() {
        return _formula;
    }

    /** @return the command we were analyzing */
    public Command getCommand() { return _command; }

    private String _getShortName(String name_) {
        return _shortener.getShortName(name_);
    }

    public String getShortName(String name_) {
        return _getShortName(name_);
    }

    /** @return <code>true</code> if a leaf expression
     * is a skolem constant, <code>false</code> otherwise
     */
    private boolean _isSkolem(LeafExpr leafExpr_) {
        return _translator.isSkolemConstant(leafExpr_.getLeafId());

        //return (leafExpr_.nodeString().indexOf(NAME_SEPARATOR) != -1)
        //&& (leafExpr_.nodeString().indexOf("@@") == -1);
    }

    private void _addSigsAndSkolemConstants(
                        Map exprsToTransls_,
                        boolean[] solution_) {
    Iterator entryIter = exprsToTransls_.entrySet().iterator();
    while (entryIter.hasNext()) {
        Map.Entry entry = (Map.Entry) entryIter.next();
        LeafExpr leafExpr = (LeafExpr) entry.getKey();
        ExprTransl leafTransl = (ExprTransl) entry.getValue();
        if (_isSkolem(leafExpr)) { // skolem constant
            _addSkolemConstant(leafExpr, leafTransl, solution_);
        } else {
            RelationType leafType = leafExpr.getType().toRelationType();
            if (leafType.arity() == 1) { // sig
                _addSig(leafExpr, leafTransl, solution_);
            }
        }
    }
    // sort the sigs in alphabetical order
    Collections.sort(_sigs);
    }

    private void _addSig(
             LeafExpr leafExpr_,
             ExprTransl leafTransl_,
             boolean[] solution_) {
    Dbg.chk(leafExpr_.getType().toRelationType().arity() == 1);
    String sigString = _getShortName(leafExpr_.nodeString());
    Dbg.chk(sigString);
    // add to _sigs
    _sigs.add(sigString);
    // add to _sigsToBasicTypes
    BasicType basicType = (BasicType) leafExpr_.getType().toRelationType().getBasicTypeAt(0);
    _sigsToBasicTypes.put(sigString, basicType);
    // get atoms
    //leafTransl_.setType(leafExpr_.getType().toRelationType());
    String valueString = leafTransl_.interpret(solution_);
    //Dbg.info(sigString);
    //Dbg.info(valueString);
    List atomList = _toList(valueString);
    // add to _sigsToAtoms
    _sigsToAtoms.put(sigString, atomList);
    // add to _atomsToSigs if sig is basic type
    if (leafExpr_.nodeString().equals(basicType.toExpr().nodeString())) {
        Iterator atomIter = atomList.iterator();
        while (atomIter.hasNext()) {
        String atom = (String) atomIter.next();
        _atomsToSigs.put(atom, sigString);
        }
    }
    }

    private void _addSkolemConstant(
                    LeafExpr leafExpr_,
                    ExprTransl leafTransl_,
                    boolean[] solution_) {
    // add to _skolemToTypes map
    String skolemString = _getShortName(leafExpr_.nodeString());
    Dbg.chk(skolemString);
    RelationType leafType = leafExpr_.getType().toRelationType();
    _skolemToTypes.put(skolemString, leafType);
    // add to _skolemToValues map
    //leafTransl_.setType(leafExpr_.getType().toRelationType());
    String valueString = leafTransl_.interpret(solution_);
    _skolemToValues.put(
                skolemString,
                _toTupleList(valueString, leafType.arity(), null));
    }

    private void _addFields(Map exprsToTransls_, boolean[] solution_) {
    // first, associate each sig with a field mapping
    // and each atom with a relation mapping
    Iterator signameIter = allSigs().iterator();
    while (signameIter.hasNext()) {
        String sigString = (String) signameIter.next();
        _sigsToFieldTypes.put(sigString, new HashMap());
        Iterator atomIter = atomsOfSig(sigString).iterator();
        while (atomIter.hasNext()) {
        _atomsToRelationValues.put(atomIter.next(), new HashMap());
        }
    }
    // now, find and add fields
    Iterator entryIter = exprsToTransls_.entrySet().iterator();
    while (entryIter.hasNext()) {
        Map.Entry entry = (Map.Entry) entryIter.next();
        LeafExpr leafExpr = (LeafExpr) entry.getKey();
        ExprTransl leafTransl = (ExprTransl) entry.getValue();
        if (!_isSkolem(leafExpr)) {
        RelationType leafType = leafExpr.getType().toRelationType();
        if (leafType.arity() > 1) { // a field
            _addField(leafExpr, leafTransl, solution_);
        }
        }
    }
    }

    private void _addField(
               LeafExpr leafExpr_,
               ExprTransl leafTransl_,
               boolean[] solution_) {
        // add to _sigsToFieldTypes mapping
        String fieldString = leafExpr_.nodeString();
        if (fieldString.indexOf("$") != -1) {
            fieldString = fieldString.substring(fieldString.indexOf("$") + 1, fieldString.length());
        }

        RelationType fieldType = leafExpr_.getType().toRelationType();
        // get sig by looking at first basic type
        BasicType basicType = fieldType.getBasicTypeAt(0);
        String sigString = _getShortName(basicType.toString());
        Dbg.chk(_sigsToFieldTypes.containsKey(sigString));
        String globalRelName = sigString + "$" + fieldString;
        // add to _relationsToRelationTypes
        _relationsToRelationTypes.put(globalRelName, fieldType);
        // get rid of the sig type from the relation type
        RelationType storedFieldType = null;
        try {
            storedFieldType = (new RelationType(basicType)).join(fieldType);
        } catch (Exception e) {
            Dbg.fatal("shouldn't happen");
        }
        ((Map) _sigsToFieldTypes.get(sigString)).put(fieldString, storedFieldType);
        //leafTransl_.setType(leafExpr_.getType().toRelationType());
        String valString = leafTransl_.interpret(solution_);
        // add to _relationsToTuples mapping
        _relationsToTuples.put(
                   globalRelName,
                   _toTupleList(valString, fieldType.arity(), null));
        // add to _atomsToRelationValues mapping
        Iterator atomIter = atomsOfSig(sigString).iterator();
        while (atomIter.hasNext()) {
            String atom = (String) atomIter.next();
            Dbg.chk(_atomsToRelationValues.containsKey(atom));
            ((Map) _atomsToRelationValues.get(atom)).put(
                             fieldString,
                             _toTupleList(valString, storedFieldType.arity(), atom));
        }
    }

    private List _toList(String valString_) {
        int index = 2;
        List atomList = new ArrayList();
        while (valString_.charAt(index) == '(') {
            index++;
            atomList.add(valString_.substring(index, valString_.indexOf(')', index)));
            index = valString_.indexOf(')', index) + 2;
        }
        return atomList;
    }

    private List _toTupleList(String valString_, int tupleSize_, String first_) {
    Dbg.chk(tupleSize_ > 0);
    // skip "{ " in value string
    int index = 2;
    List tupleList = new ArrayList();
    while (valString_.charAt(index) == '(') {
        boolean addTuple = true;
        index++;
        String[] curTuple = new String[tupleSize_];
        if (first_ != null) {
        // only add tuple of first element matches
        // first_
        addTuple =
                first_.equals(valString_.substring(index, valString_.indexOf(' ', index)));
        index = valString_.indexOf(' ', index) + 1;
        }
        for (int i = 0; i < tupleSize_; i++) {
        int atomEnd =
                (i == tupleSize_ - 1)
                ? valString_.indexOf(')', index)
                : valString_.indexOf(' ', index);
        curTuple[i] = valString_.substring(index, atomEnd);
        index = atomEnd + 1;
        }
        if (addTuple) {
        tupleList.add(curTuple);
        }
        index++;
    }
    return tupleList;
    }

    /**
       Module that detects which names in a solution can be shortened
       without creating ambiguity.  Signature names are shortened by
       removing the path of qualified names, leaving the final identifier
       seen in the declaration.  Skolem constants are shortened by removing
       the unique number at the end of the constant.
    */
    private final class NameShortener {

        /** set of {@link alloy.ast.QualifiedName qualified names} of
            signatures which can be shortened without creating ambiguity */
        private Set _canBeShortened = new HashSet();

        /** set of {@link alloy.ast.Id unqualified names} which are shared
            by more than one signature */
        private Set _sharedIds = new HashSet();

        /** set of {@link String skolem constant names} which can be
            shortened without causing ambiguity */
        private Set _skolemShortened = new HashSet();

        /** set of {@link String shortened skolem constant names} which
            cannot be used because they cause ambiguity */
        private Set _skolemShared = new HashSet();

        /** a Map from String signature and skolem constant
            full names to either the same full name or a shortened
            name if shortening is possible */
        private Map _nameToShortName = new HashMap();

        NameShortener(Map exprsToTransls_) {
            // detect which names can be shortened in first pass
            Iterator exprIter = exprsToTransls_.keySet().iterator();
            while (exprIter.hasNext()) {
            LeafExpr leafExpr = (LeafExpr) exprIter.next();
            if (_isSkolem(leafExpr)) {
                // skolem constant
                _detectSharedSkolem(leafExpr);
            } else if (leafExpr.getType().toRelationType().arity() == 1) {
                _detectSharedIds((SigExpr) leafExpr);
            }
            }
            // create short names in second pass
            exprIter = exprsToTransls_.keySet().iterator();
            while (exprIter.hasNext()) {
            LeafExpr leafExpr = (LeafExpr) exprIter.next();
            if (_isSkolem(leafExpr)) {
                // skolem constant
                _createShortSkolemName(leafExpr);
            } else if (leafExpr.getType().toRelationType().arity() == 1) {
                _createShortSigName((SigExpr) leafExpr);
            }
            }
        }

        public String getShortName(String name_) {
                if (_nameToShortName.containsKey(name_))
                    return (String) _nameToShortName.get(name_);
                return name_;
        }

        /** detect whether the skolem constant has a name that
            can be shortened, given the skolem constants already seen.
            note that we may detect an ambiguity for this skolem shorten
            name when checking a later skolem constant.
        */
        private void _detectSharedSkolem(LeafExpr leafExpr_) {
            String fullName = leafExpr_.nodeString();
            // skolem constant with number at end removed
            String shortName = _shortenSkolem(fullName);
            // if already detected to be ambiguous, just return
            if (_skolemShared.contains(shortName))
            return;
            if (_skolemShortened.contains(shortName)) {
            // if some other skolem constant has the
            // same short name, remove it from the
            // set of shortenable names
            _skolemShortened.remove(shortName);
            // add short name to set of those
            // detected to be ambiguous
            _skolemShared.add(shortName);
            } else {
            // for now, name is shortenable, so
            // add to set of shortenable names
            _skolemShortened.add(shortName);
            }
        }

        private String _shortenSkolem(String fullName) {
            return fullName.substring(fullName.indexOf("@") + 1, fullName.length());
        }

        /** add skolem constant name to {@link #_nameToShortName} mapping,
            mapped to short name if possible */
        private void _createShortSkolemName(LeafExpr leafExpr_) {
            String fullName = leafExpr_.nodeString();
            String shortName = _shortenSkolem(fullName);
            _nameToShortName.put(
                     fullName,
                     _skolemShortened.contains(shortName) ? shortName : fullName);
        }

        /** detect whether a signature has a name that
            can be shortened, given the signature names already seen.
            note that we may detect an ambiguity for this short sig name
            when checking a later sig
        */
        private void _detectSharedIds(SigExpr sigExpr_) {
            QualifiedName qName = sigExpr_.getSig();
            Id id = qName.getId();
            if (_canBeShortened.contains(qName))
            return;
            if (_sharedIds.contains(id))
            return;
            for (Iterator iter = _canBeShortened.iterator(); iter.hasNext();) {
            QualifiedName curQName = (QualifiedName) iter.next();
            if (id.equals(curQName.getId())) {
                // remove curQName from set
                iter.remove();
                // add id to set of shared ids
                _sharedIds.add(id);
                return;
            }
            }
            // qName has unique id for now
            _canBeShortened.add(qName);
        }

        /** create the short name for a signature, possibly
            using short names for its parameter types if
            it has been instantiated */
        private void _createShortSigName(SigExpr sigExpr_) {
            String fullName = sigExpr_.nodeString();
            //Dbg.info("adding short name for " + fullName);
            // if name has already been created, return
            if (_nameToShortName.containsKey(fullName))
                return;
            QualifiedName sigName = sigExpr_.getSig();
            String shortName =
                _canBeShortened.contains(sigName)
                ? sigName.getId().nodeString()
                : sigName.nodeString();
            _nameToShortName.put(fullName, shortName);
        }
    } // NameShortener



    /** saves the instance data using a PrintWriter. */
    public void saveInstance (PrintWriter writer) {
        writer.println ("Version 1 Instance File");
        writer.println ("# of vars:");
        writer.println (_solution.length);
        writer.println ("values:");

        for (int i = 0; i < _solution.length; i++) {
            writer.println (_solution[i]);
        }
        writer.flush();
    }


    /** loads the instance data using a BufferedReader. */
    public boolean loadInstance (BufferedReader reader) {
        int cntr;

        try {
            if (!reader.readLine().equals("Version 1 Instance File"))
            return false;

            reader.readLine();  // # of vars
            int numVars = Integer.parseInt(reader.readLine());
            reader.readLine(); // values

            for (cntr = 0; cntr < _solution.length; cntr++) {
            _solution[cntr] = Boolean.valueOf(reader.readLine()).booleanValue();
            }
        }
        catch (Exception ex) {
            return false;
        }

        return true;
    }

    /* (non-Javadoc)
     * @see alloy.api.SolutionData#getInstance()
     */
    public VizInstance getVizInstance() {
        return _instance;
    }

    /* (non-Javadoc)
     * @see alloy.api.SolutionData#mapAtomName(java.lang.String)
     */
    public String mapAtomName(String atom) {
        return atom;
    }

    /* (non-Javadoc)
     * @see alloy.api.SolutionData#setInstance(alloy.viz.alloyviz.Instance)
     */
    public void setVizInstance(VizInstance instance) {
        _instance = instance;
    }

    /**
     * Return the {@link BasicType} corresponding to Int, or <code>null</code>
     * if Int wasn't used in the model.
     * @see #getIntAtomValue
     */
    public BasicType getIntType() { return _translator.getIntType(); }

    /**
     * Get the integer associated with the i'th integer atom.
     * Assumes that integers were used in the model.
     * @param intAtomIdx_ the index of the integer atom; must have
     *        0 <= intAtomIdx_ < getASTInfo().getIntType().getScope().
     * @throws IndexOutOfBoundsException if atom index is invalid or if
     *         integers weren't used in the model.
     * @see ASTInfo#getIntType
     */
    public long getIntAtomValue(int intAtomIdx_) throws IndexOutOfBoundsException {
        BasicType intType = getIntType();
        if (intType == null)
            throw new IndexOutOfBoundsException("integers not used in the model");
        if (intAtomIdx_ < 0 || intAtomIdx_ >= intType.getScope())
            throw new IndexOutOfBoundsException("invalid index of Int atom");
        return _translator.getRelationAllocator().getIntAtomTransl(intAtomIdx_).interpretAsInt(_solution);
    }
}
